COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
CS258                         PROBLEM SET			WINTER 1979

.ITEM ← 0

#. Define

	%2flat[x,u] ← qif qat x qthen x.u qelse flat[qa x,flat[qd x, u]]%1.

Prove that ⊗flat is total.

#. Prove the termination of the 91-function defined by

	%2f n ← qif n greater 100 qthen n-10 else f(f(n + 11)%1.

#. %2fix e%1 is an algorithm to transform a compound conditional
expression ⊗e into an equivalent conditional expression that has only
atomic propositional parts in the expression as a whole and its
subexpressions.  It uses the rule

	%2qif (qif p qthen q qelse r) qthen a qelse b = qif p qthen (qif
q qelse a qelse b) qelse (qif r qthen a qelse b)%1

as long as it is applicable.  It uses the abstract syntax of conditional
expressions which satisfies the following equations:

	%2prop("if p qthen a qelse b") = "p"

	%2antec("if p qthen a qelse b") = "a"

	%2conseq("if p qthen a qelse b") = "c"

	%2mkcond("p","a","b") = "qif p qthen a qelse b".

Write the algebraic axioms and the induction schema satisfied by
the functions ⊗prop, ⊗antec, ⊗conseq and %2mkcond%1.

Prove the termination of the algorithm ⊗fix by
inventing a suitable rank function.

	%2fix e ← qif qat e qthen e qelse α{fix antec e, fix conseq eα}
[λa b.qif qat prop e qthen e qelse fix mkcond(prop prop e, mkcond(antec prop e,
antec e,conseq e), mkcond(conseq prop e,antec e,conseq e))]%1.

#. A term ⊗t may be substituted for a variable ⊗x in an expression ⊗e provided
no variable free in ⊗t will be captured by a quantifier in ⊗e.  Suppose
that the expressions are in Lisp form and that the only quantifiers are
∀, ∃ and λ, used in the forms (∀ <varlist> <wff>), (∃ <varlist> <wff>) and
(λ <varlist> <term>), write the Lisp predicate ⊗freefor[x,t,e] and
prove that it is total.  Prove that if %2x_=_t%1 in some interpretation
and %2freefor(x,t,e)%1, then %2subst(t,x,e)_=_t%1 in that interpretation.